the_w:World, e:E. kind(e)  Knd 

latex

Definitions	x:A. B(x), t  T, kind(e), P  Q, Prop
Lemmas	w-kind wf, w-loc wf, w-act wf, w-action wf, not wf, assert wf, w-isnull wf, w-E wf, world wf, w-act-not-null